<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Issue2604</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">-- Andreas, 2017-06-16, issue #2604:</a>
<a id="38" class="Comment">-- Symbolic anchors in generated HTML.</a>

<a id="78" class="Keyword">module</a> <a id="85" href="Issue2604.html" class="Module">Issue2604</a> <a id="95" class="Keyword">where</a>

<a id="test1"></a><a id="102" href="Issue2604.html#102" class="Function">test1</a> <a id="108" class="Symbol">:</a> <a id="110" href="Agda.Primitive.html#388" class="Primitive">Set₁</a>  <a id="116" class="Comment">-- Symbolic anchor</a>
<a id="135" href="Issue2604.html#102" class="Function">test1</a> <a id="141" class="Symbol">=</a> <a id="143" href="Issue2604.html#157" class="Function">bla</a>
  <a id="149" class="Keyword">where</a>
  <a id="157" href="Issue2604.html#157" class="Function">bla</a> <a id="161" class="Symbol">=</a> <a id="163" href="Agda.Primitive.html#388" class="Primitive">Set</a>   <a id="169" class="Comment">-- Position anchor</a>

<a id="test2"></a><a id="189" href="Issue2604.html#189" class="Function">test2</a> <a id="195" class="Symbol">:</a> <a id="197" href="Agda.Primitive.html#388" class="Primitive">Set₁</a>  <a id="203" class="Comment">-- Symbolic anchor</a>
<a id="222" href="Issue2604.html#189" class="Function">test2</a> <a id="228" class="Symbol">=</a> <a id="230" href="Issue2604.html#244" class="Function">bla</a>
  <a id="236" class="Keyword">where</a>
  <a id="244" href="Issue2604.html#244" class="Function">bla</a> <a id="248" class="Symbol">=</a> <a id="250" href="Agda.Primitive.html#388" class="Primitive">Set</a>   <a id="256" class="Comment">-- Position anchor</a>

<a id="test3"></a><a id="276" href="Issue2604.html#276" class="Function">test3</a> <a id="282" class="Symbol">:</a> <a id="284" href="Agda.Primitive.html#388" class="Primitive">Set₁</a>  <a id="290" class="Comment">-- Symbolic anchor</a>
<a id="309" href="Issue2604.html#276" class="Function">test3</a> <a id="315" class="Symbol">=</a> <a id="317" href="Issue2604.html#340" class="Function">bla</a>
  <a id="323" class="Keyword">module</a> <a id="M"></a><a id="330" href="Issue2604.html#330" class="Module">M</a> <a id="332" class="Keyword">where</a>
  <a id="M.bla"></a><a id="340" href="Issue2604.html#340" class="Function">bla</a> <a id="344" class="Symbol">=</a> <a id="346" href="Agda.Primitive.html#388" class="Primitive">Set</a>  <a id="351" class="Comment">-- Symbolic anchor</a>

<a id="371" class="Keyword">module</a> <a id="NamedModule"></a><a id="378" href="Issue2604.html#378" class="Module">NamedModule</a> <a id="390" class="Keyword">where</a>
  <a id="NamedModule.test4"></a><a id="398" href="Issue2604.html#398" class="Function">test4</a> <a id="404" class="Symbol">:</a> <a id="406" href="Agda.Primitive.html#388" class="Primitive">Set₁</a>  <a id="412" class="Comment">-- Symbolic anchor</a>
  <a id="433" href="Issue2604.html#398" class="Function">test4</a> <a id="439" class="Symbol">=</a> <a id="441" href="Issue2604.html#340" class="Function">M.bla</a>

<a id="448" class="Keyword">module</a> <a id="455" href="Issue2604.html#455" class="Module">_</a> <a id="457" class="Keyword">where</a>
  <a id="465" href="Issue2604.html#465" class="Function">test5</a> <a id="471" class="Symbol">:</a> <a id="473" href="Agda.Primitive.html#388" class="Primitive">Set₁</a>  <a id="479" class="Comment">-- Position anchor</a>
  <a id="500" href="Issue2604.html#465" class="Function">test5</a> <a id="506" class="Symbol">=</a> <a id="508" href="Issue2604.html#340" class="Function">M.bla</a>

<a id="515" class="Comment">-- Testing whether # in anchors confuses the browsers.</a>
<a id="570" class="Comment">-- Not Firefox 54.0, at least (Andreas, 2017-06-20).</a>
<a id="623" class="Comment">-- However, the Nu Html Checker complains (someone else, later).</a>

<a id="#"></a><a id="689" href="Issue2604.html#689" class="Function">#</a> <a id="691" class="Symbol">:</a> <a id="693" href="Agda.Primitive.html#388" class="Primitive">Set₁</a>
<a id="698" href="Issue2604.html#689" class="Function">#</a> <a id="700" class="Symbol">=</a> <a id="702" href="Agda.Primitive.html#388" class="Primitive">Set</a>

<a id="#a"></a><a id="707" href="Issue2604.html#707" class="Function">#a</a> <a id="710" class="Symbol">:</a> <a id="712" href="Agda.Primitive.html#388" class="Primitive">Set₁</a>
<a id="717" href="Issue2604.html#707" class="Function">#a</a> <a id="720" class="Symbol">=</a> <a id="722" href="Issue2604.html#689" class="Function">#</a>

<a id="b#"></a><a id="725" href="Issue2604.html#725" class="Function">b#</a> <a id="728" class="Symbol">:</a> <a id="730" href="Agda.Primitive.html#388" class="Primitive">Set₁</a>
<a id="735" href="Issue2604.html#725" class="Function">b#</a> <a id="738" class="Symbol">=</a> <a id="740" href="Issue2604.html#707" class="Function">#a</a>

<a id="##"></a><a id="744" href="Issue2604.html#744" class="Function">##</a> <a id="747" class="Symbol">:</a> <a id="749" href="Agda.Primitive.html#388" class="Primitive">Set₁</a>
<a id="754" href="Issue2604.html#744" class="Function">##</a> <a id="757" class="Symbol">=</a> <a id="759" href="Issue2604.html#725" class="Function">b#</a>

<a id="763" class="Comment">-- The href attribute values #A and #%41 are (correctly?) treated as</a>
<a id="832" class="Comment">-- pointers to the same destination by Firefox 54.0. To point to %41</a>
<a id="901" class="Comment">-- one should use #%2541.</a>

<a id="A"></a><a id="928" href="Issue2604.html#928" class="Function">A</a> <a id="930" class="Symbol">:</a> <a id="932" href="Agda.Primitive.html#388" class="Primitive">Set₁</a>
<a id="937" href="Issue2604.html#928" class="Function">A</a> <a id="939" class="Symbol">=</a> <a id="941" href="Agda.Primitive.html#388" class="Primitive">Set</a>

<a id="%41"></a><a id="946" href="Issue2604.html#946" class="Function">%41</a> <a id="950" class="Symbol">:</a> <a id="952" href="Agda.Primitive.html#388" class="Primitive">Set₁</a>
<a id="957" href="Issue2604.html#946" class="Function">%41</a> <a id="961" class="Symbol">=</a> <a id="963" href="Issue2604.html#928" class="Function">A</a>

<a id="966" class="Comment">-- Ampersands may need to be encoded in some way. The blaze-html</a>
<a id="1031" class="Comment">-- library takes care of encoding id attribute values, and we manually</a>
<a id="1102" class="Comment">-- replace ampersands with %26 in the fragment parts of href attribute</a>
<a id="1173" class="Comment">-- values.</a>

<a id="&amp;amp"></a><a id="1185" href="Issue2604.html#1185" class="Function">&amp;amp</a> <a id="1190" class="Symbol">:</a> <a id="1192" href="Agda.Primitive.html#388" class="Primitive">Set₁</a>
<a id="1197" href="Issue2604.html#1185" class="Function">&amp;amp</a> <a id="1202" class="Symbol">=</a> <a id="1204" href="Agda.Primitive.html#388" class="Primitive">Set</a>

<a id="&amp;lt"></a><a id="1209" href="Issue2604.html#1209" class="Function">&amp;lt</a> <a id="1213" class="Symbol">:</a> <a id="1215" href="Agda.Primitive.html#388" class="Primitive">Set₁</a>
<a id="1220" href="Issue2604.html#1209" class="Function">&amp;lt</a> <a id="1224" class="Symbol">=</a> <a id="1226" href="Issue2604.html#1185" class="Function">&amp;amp</a>

<a id="1232" class="Comment">-- Test of fixity declarations. The id attribute value for the</a>
<a id="1295" class="Comment">-- operator in the fixity declaration should be unique.</a>

<a id="1352" class="Keyword">infix</a> <a id="1358" class="Number">0</a> <a id="1360" href="Issue2604.html#1368" class="Function Operator">_%42∀_</a>

<a id="_%42∀_"></a><a id="1368" href="Issue2604.html#1368" class="Function Operator">_%42∀_</a> <a id="1375" class="Symbol">:</a> <a id="1377" href="Agda.Primitive.html#388" class="Primitive">Set₁</a>
<a id="1382" href="Issue2604.html#1368" class="Function Operator">_%42∀_</a> <a id="1389" class="Symbol">=</a> <a id="1391" href="Agda.Primitive.html#388" class="Primitive">Set</a>

<a id="1396" class="Comment">-- The following two variants of the character Ö should result in</a>
<a id="1462" class="Comment">-- distinct links.</a>

<a id="Ö"></a><a id="1482" href="Issue2604.html#1482" class="Function">Ö</a> <a id="1484" class="Symbol">:</a> <a id="1486" href="Agda.Primitive.html#388" class="Primitive">Set₁</a>
<a id="1491" href="Issue2604.html#1482" class="Function">Ö</a> <a id="1493" class="Symbol">=</a> <a id="1495" href="Agda.Primitive.html#388" class="Primitive">Set</a>

<a id="Ö"></a><a id="1500" href="Issue2604.html#1500" class="Function">Ö</a> <a id="1503" class="Symbol">:</a> <a id="1505" href="Agda.Primitive.html#388" class="Primitive">Set₁</a>
<a id="1510" href="Issue2604.html#1500" class="Function">Ö</a> <a id="1513" class="Symbol">=</a> <a id="1515" href="Issue2604.html#1482" class="Function">Ö</a>
</pre></body></html>